.DEVICE XGP
.FONT 4 "BASB30"
.FONT 3 "BASI30"
.FONT 2 "BDR30"
.FONT 1 "BDR30"
.EVENLEFTBORDER←ODDLEFTBORDER←1000
.PAGE FRAME 52 HIGH 83 WIDE;
.AREA TEXT LINES 4 TO 50;
.TITLE AREA HEADING LINES 1 TO 3;
.PLACE TEXT;
.EVERY HEADING(,,{PAGE});
.BEGIN NOFILL
.VARIABLE CHW
.CHW ← CHARW
.TURN OFF "βα#\←∞↑↓∪"
.TURN ON "∂{%"
.TURN ON "/" FOR "α"
.AT "∂∂(" CH ")" ⊂ CHARW←CH}∂(2){CHARW←CHW ⊃


∂∂(48)%βcommutative%α %βop%α ← %βop%α ε (PLUS TIMES UNION INTERSECTION)



∂∂(48)%βinst%α[%βe%α, %βm%α, %βp%α] ← 
∂∂(80)%∧if%α %βp%α %∧eq %αNO %∧then%α %βp
∂∂(80)%∧else if%α %∧at %βm%α %∧then%α 
∂∂(112)[%∧if%α %βisvar%α %βm%α %∧then%α 
∂∂(144)/{%βassoc%α[%βm%α, %βp%α]}[λ%βw%α. %∧if%α %∧n %βw%α %∧then%α [%βm%α . %βe%α] . %βp%α %∧else if%α %βequal%α[%∧d %βw%α, %βe%α] %∧then%α %βp%α %∧else%α NO]
∂∂(121)%∧else if%α %βm%α %∧eq %βe%α %∧then%α %βp
∂∂(121)%∧else%α NO]
∂∂(80)%∧else if%α %∧at %βe%α %∧then%α NO
∂∂(80)%∧else if%α %βcommutative%α %∧a %βm%α %∧then%α [%∧if%α %∧at %βe%α %∧then%α NO %∧else%α %βcomminst%α[%∧d %βe%α, %∧d %βm%α, %βinst%α[%∧a %βe%α, %∧a %βm%α, %βp%α], %2NIL%α]]
∂∂(80)%∧else%α %βinst%α[%∧d %βe%α, %∧d %βm%α, %βinst%α[%∧a %βe%α, %∧a %βm%α, %βp%α]]



∂∂(48)%βisvar%α %βm%α ← %βm%α ε (U V W X Y Z)



∂∂(48)%βsublis%α[%βe%α, %βp%α] ← 
∂∂(80)%∧if%α %∧at %βe%α %∧then%α /{%βassoc%α[%βe%α, %βp%α]}[λ%βw%α. %∧if%α %∧n %βw%α %∧then%α %βe%α %∧else%α %∧d %βw%α]
∂∂(80)%∧else%α /{%βsublis%α[%∧a %βe%α, %βp%α], %βsublis%α[%∧d %βe%α, %βp%α]}[λ%βx%α, %βy%α. %∧if%α %βx%α %∧eq a %βe%α ∧ %βy%α %∧eq d %βe%α %∧then%α %βe%α %∧else%α %βx%α . %βy%α]



∂∂(48)%βcomminst%α[%βlexp%α, %βlpat%α, %βa%α, %βu%α] ← 
∂∂(80)%∧if%α %βa%α %∧eq %αNO %∧then%α NO
∂∂(80)%∧else if%α %∧at %βlpat%α %∧then%α 
∂∂(112)[%∧if%α %βisvar%α %βlpat%α %∧then%α 
∂∂(144)/{%βassoc%α[%βlpat%α, %βa%α]}[λ%βw%α. 
∂∂(176)%∧if%α %∧n %βw%α %∧then%α [%βlpat%α . [%βlexp%α * %βu%α]] . %βa%α %∧else if%α %βequal%α[%∧d %βw%α, %βlexp%α] ∧ %∧n %βu%α %∧then%α %βa%α %∧else%α NO]
∂∂(121)%∧else if%α %βlpat%α %∧eq %βlexp%α %∧then%α %βa
∂∂(121)%∧else%α NO]
∂∂(80)%∧else if%α %∧n %βlexp%α %∧then%α NO
∂∂(80)%∧else%α /{%βinst%α[%∧a %βlexp%α, %∧a %βlpat%α, %βa%α]}[λ%βw%α. 
∂∂(112)%∧if%α %βw%α %∧eq %αNO %∧then%α %βcomminst%α[%∧d %βlexp%α, %βlpat%α, %βa%α, %∧a %βlexp%α . %βu%α]
∂∂(112)%∧else%α /{%βcomminst%α[%βu%α * %∧d %βlexp%α, %∧d %βlpat%α, %βw%α, %2NIL%α]}[λ%βz%α. 
∂∂(144)%∧if%α %βz%α %∧eq %αNO %∧then%α %βcomminst%α[%∧d %βlexp%α, %βlpat%α, %βa%α, %∧a %βlexp%α . %βu%α] %∧else%α %βz%α]]

.END